COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out) 
C00012 ENDMK
C⊗;
(wipe-out) 
(proof lispax) 

;;;declarations: note that t and nil are not declared - ekl knows about them
;;;since they are attached, we don't need to say things like null nil etc.

(decl car (unaryname: car) (type: |ground→ground|) (syntype: constant)
(bindingpower: 950))

(decl cdr (unaryname: cdr) (type: |ground→ground|) (syntype: constant)
(bindingpower: 950))

(decl atom (unaryname: atom) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

(decl null (unaryname: null) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

(decl listp (unaryname: listp) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

(decl alistp (unaryname: alistp) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

(decl sexp (unaryname: sexp) (type: |ground→truthval|) (syntype: constant)
(bindingpower: 750))

(decl (u v w) (type: |ground|) (sort: |listp|))

(decl (x y z) (type: |ground|) (sort: |sexp|))

(decl (xa ya za) (type: |ground|) (sort: |atom|))

(decl (phi) (type: |ground→truthval|))

(decl cons (type: |(ground⊗ground)→ground|) (syntype: constant) (infixname: |.|)
(prefixname: cons) (bindingpower: 850))

;;;basic axioms and sort info

(axiom |∀xa.sexp(xa)|)
(label simpinfo)

(axiom |∀u.sexp u|)
(label simpinfo)

(axiom |∀x u.listp x.u|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ listp cdr u|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ sexp car u|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ sexp car x|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ sexp cdr x|)
(label simpinfo)

(axiom |∀x y.sexp x.y|)
(label simpinfo)

(axiom |∀x y.¬atom x.y|)
(label simpinfo)

(axiom |∀x u.¬null x.u|)
(label simpinfo)

(axiom |∀u.null u ⊃ u = nil|)
(label simpinfo)

(axiom |∀x y.car (x.y) = x|)
(label simpinfo)

(axiom |∀x y.cdr (x.y) = y|)
(label simpinfo)

(axiom |car nil = nil|)
(label simpinfo)

(axiom |cdr nil = nil|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ (car u.cdr u=u)|)
(label simpinfo) (label cons_car_cdr)

(axiom |∀x.¬atom x ⊃ (car x.cdr x=x)|)
(label simpinfo) (label cons_car_cdr)

;;;induction

(axiom |∀phi.phi(nil)∧(∀x u.phi(u)⊃phi(x.u))⊃(∀u.phi(u))|)
(label listinduction)

(decl pars (type: |ground*|))
(decl (df df1 df2) (type: |ground⊗ground*→ground*|))
(decl nilcase (type: |ground*→ground*|))
(axiom
|∀df nilcase def.(∃fun.(∀pars x u.fun(nil,pars)=nilcase(pars)∧
                               fun(x.u,pars)=def(x,u,fun(u,df(x,pars)),pars)))|)
(label listinductiondef)

(axiom |∀phi.(∀x.atom x ⊃ phi(x))∧(∀x y.phi(x)∧phi(y)⊃phi(x.y))⊃(∀x.phi(x))|)
(label sexpinduction)

(axiom
|∀atomcase defsexp df1 df2.
∃fun. ∀pars x y z.
(atom z ⊃ fun(z,pars)=atomcase(z,pars))∧
(fun(x.y,pars)=defsexp(x,y,fun(x,df1(x,y,pars)),fun(y,df2(x,y,pars)),pars))|)
(label sexpinductiondef)

;a high order definition schema when above is insufficient

(decl (arb arb1 arb2) (type: |?arbitrary|))
(decl bigfun (type: |ground⊗ground⊗@arb⊗@arb→@arb|))
(decl (defined_fun atom_fun) (type: |ground→@arb|))

;this is the primitive recursive schema for definition on  ALL
;higher type functionals:
;note the use of the variable type in declarations;
;in this way we can specialize to ANY type.

(axiom
|∀bigfun atom_fun.∃defined_fun.∀x y.(atom x ⊃ defined_fun(x)=atom_fun(x))∧
                                 (defined_fun(x.y)=
                                   bigfun(x,y,defined_fun(x),defined_fun(y)))|)
(label high_order_definition)
 
;;; lists of variable numbers of arguments don't require special treatment,
;;; since we have list types now

(decl list (type: |ground* → ground|) (syntype: constant))
(decl lst (type: |ground*|))

(axiom |list() = nil|)
(label simpinfo)

(axiom |∀lst.listp(list(lst))|)
(label simpinfo)

(axiom |∀x lst.list(x,lst) = x.list(lst)|)
(label simpinfo)
(label listdef)

;;; this is lisp's append.  while it can be proved associative, it
;;; is convenient in proofs of other theorems to have it declared
;;; associative.
 
(decl append (type: |ground⊗ground⊗(ground*)→ground|) (syntype: constant)
  (associativity: both) (infixname: *) (bindingpower: 840))

(defax append |∀x u v.nil*v=v∧(x.u)*v=x.(u*v)|)
(label appendef) (label simpinfo)

(axiom |∀u v.listp(u*v)|)
(label simpinfo) (label listappend)

(axiom |∀u.u*nil=u|)
(label simpinfo)

(axiom |∀x v.(x.nil)*v=x.v|)
(label simpinfo)

;;;map functions on lists

(decl (allp somep) (syntype: constant) (type: |(@phi)⊗ground→truthval|))
(defax allp |∀phi x u.allp(phi,nil)∧
                  allp(phi,x.u)=if phi(x) then allp(phi,u) else false|)
(label allpdef)

(defax somep |∀phi x u.¬somep(phi,nil)∧
                   somep(phi,x.u)=if phi(x) then true else somep(phi,u)|)
(label somepdef)

(defax mapcar |∀fn x u.mapcar(fn,nil)=nil∧mapcar(fn,x.u)=fn(x).mapcar(fn,u)|)
(label mapcardef)

(decl (alist) (type: ground) (sort: alistp))
(axiom |∀alist. listp alist|)
(label simpinfo) 

(axiom |∀u.alistp u ≡ (¬null u ⊃
                       ¬atom car u∧atom car (car u)∧alistp(cdr u))|)
(label alistdef1)

(axiom |∀xa y alist.alistp nil ∧ alistp (xa.y).alist|)
(label alistdef) (label simpinfo)

(decl assoc (type:  |ground⊗ground → ground|) (syntype: constant))

(defax assoc |∀x xa y alist.
          assoc(x,nil)=nil∧
          assoc(x,(xa.y).alist)=(if x=xa then xa.y else assoc(x,alist))|)
(label assocdef)

(axiom |∀x alist.sexp assoc(x,alist)|)
(label simpinfo)

(decl member (type: |ground⊗ground → truthval|) (syntype: constant))

(defax member |∀x y u. ¬member(x,nil)∧member(x,y.u)=(x=y∨member(x,u))|)
(label memberdef)

(decl uniqueness (type: |ground → truthval|) (syntype: constant))

(defax uniqueness |∀u x.uniqueness nil∧
                        (uniqueness(x.u)≡¬member(x,u)∧uniqueness u)|)
(label uniquenessdef)

(ue (phi |λu.sexp car(u)|) listinduction)
(label simpinfo)

(ue (phi |λu.listp cdr(u)|) listinduction)
(label simpinfo)

(save-proofs lispax)